#coding=utf-8
import sympy as sym
from ttg import Truths

def is_tautology(expression):
    # 将表达式转换为符号对象
    expr = sym.sympify(expression)
    # 获取表达式中的所有符号
    symbols = expr.free_symbols
    # 将所有符号连接成字符串
    symbol_str = ', '.join(map(str, symbols))
    # 使用真值表生成器计算真值表
    tt = Truths([symbol_str, str(expr)])  # 将表达式转换为字符串
    # 检查是否为重言式
    return all(row[-1] for row in tt.as_pandas().itertuples(index=False))

# 定义符号 p, q
p, q = sym.symbols('p q')

# 输出析取三段论，中间逗号使用析取符号
result = f"{p} | {q}, {q} | {p}"
print(result)

# 判断((p -> q) & q) -> p 是否为重言式
formula = sym.Implies(sym.And(sym.Implies(p, q), q), p)
tautology_result = is_tautology(formula)
print(tautology_result)

# 验证析取三段论是否为重言式
example_formula = sym.And(sym.Or(p, q), sym.Or(q, p))
example_result = is_tautology(example_formula)
print(example_result)
